A:MsgA, b:Id, s, s0:A.state.
ma-frame-compat(A;A)
 b in dom(A.pre)
 (A.pre(b,s)  A.pre(b,x.if A:locl(b) may not read x then s0(x) else s(x) fi )) 

latex

Definitions

b, , x:A. B(x), t  T, x. t(x), Id, Knd, type List, a:A fp B(a), Top, x:AB(x), f(a), Type, x.A(x), f(x)?z, locl(a), P  Q, f(x), KindDeq, deq-member(eq;x;L), b, IdDeq, x  dom(f), p  q, if b then t else f fi , s = t, A, , left + right, P  Q, case b of inl(x) => s(x) | inr(y) => t(y), True, False, x:A  B(x), IdLnk, P & Q, z != f(x)  P(a;z), State(ds), M.ds(x), xdom(f). v=f(x)   P(x;v), (s1  s2 mod x), M.da(a), M.state, M.rframe(A.sends tfL of k on l), M.sframe(k sends <l,tg>), M.rframe(A.effect f of k on y), M.aframe(k affects x), M.frame(k affects x), M.rframe(A.pre p for a), ma-frame-compat(A;B), M:k may not read x, Valtype(da;k), a in dom(M.pre), M.pre(a,s), MsgA, P  Q, P  Q, a = b, list_accum(x,a.f(x;a);y;l), xL. P(x), (x  l), Atom$n, {x:A| B(x)} , EqDecider(T), [], <a, b>, [car / cdr], {T}, ff, Unit, eqof(d), p q, T, t.1, Dec(P), SQType(T), s ~ t, x,y. t(x;y)

Lemmas

list accum wf, bool sq, Id sq, all functionality wrt iff, implies functionality wrt iff, decidable assert, pi1 wf, assert of bor, or functionality wrt iff, squash wf, true wf, bnot thru bor, assert of band, and functionality wrt iff, assert-deq-member, not functionality wrt iff, assert-eq-id, bor wf, eqof wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bfalse wf, eq id wf, cons member, l all wf2, l member wf, ma-pre wf, not wf, bool wf, assert wf, ifthenelse wf, band wf, fpf-dom wf, id-deq wf, bnot wf, deq-member wf, Knd wf, Kind-deq wf, fpf-ap wf, locl wf, fpf-cap wf, Id wf, top wf, fpf-trivial-subtype-top